Example 8 in [Borralleras, Lucas & Rubio - CADE'02]

Summary: Ex8_BLR02

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (Extra variables)
• Positive results:
  1. Zantema's transformation (RPOS @ AProVE)
  2. Ferreira and Ribeiro's transformation (Corollary)
  3. Giesl and Middeldorp's transformation (Corollary)
  4. CSRPO

CS-TRS Ex8_BLR02 (file Ex8_BLR02.csr)

Functions:  fib sel fib1 s 0 cons add

Constructors:  s 0 cons

Variables:  N X Y XS

Arities: 

ar(fib) = 1
ar(sel) = 2
ar(fib1) = 2
ar(s) = 1
ar(0) = 0
ar(cons) = 2
ar(add) = 2

Replacement map: 

µ(fib)={1}
µ(sel)={1,2}
µ(fib1)={1,2}
µ(s)={1}
µ(0)={}
µ(cons)={1}
µ(add)={1,2}

Rules: (file Ex8_BLR02) 

fib(N) -> sel(N,fib1(s(0),s(0)))
fib1(X,Y) -> cons(X,fib1(Y,add(X,Y)))
add(0,X) -> X
add(s(X),Y) -> s(add(X,Y))
sel(0,cons(X,XS)) -> X
sel(s(N),cons(X,XS)) -> sel(N,XS)

The CS-TRS in OBJ format (file Ex8_BLR02.obj):

obj Ex8_BLR02 is
  sort S .
  op fib : S -> S .
  op sel : S S -> S .
  op fib1 : S S -> S .
  op s : S -> S .
  op 0 : -> S .
  op cons : S S -> S [strat (1 0)] .
  op add : S S -> S .
  vars N X Y XS : S .
  eq fib(N) = sel(N,fib1(s(0),s(0))) .
  eq fib1(X,Y) = cons(X,fib1(Y,add(X,Y))) .
  eq add(0,X) = X .
  eq add(s(X),Y) = s(add(X,Y)) .
  eq sel(0,cons(X,XS)) = X .
  eq sel(s(N),cons(X,XS)) = sel(N,XS) .
endo

Negative results

1. The µ-termination of Ex8_BLR02 cannot be proved by using Lucas' transformation. The TRS Ex8_BLR02_L:

       fib(N) -> sel(N,fib1(s(0),s(0)))
       fib1(X,Y) -> cons(X)
       add(0,X) -> X
       add(s(X),Y) -> s(add(X,Y))
       sel(0,cons(X)) -> X
       sel(s(N),cons(X)) -> sel(N,XS)
       

   contains extra variables.

Positive results

1. The µ-termination of Ex8_BLR02 can be proved by using Zantema's transformation. The TRS Ex8_BLR02_Z:

       fib(N) -> sel(N,fib1(0,s(0)))
       fib1(X,Y) -> cons(X,n__fib1(Y,add(X,Y)))
       add(0,X) -> X
       add(s(X),Y) -> s(add(X,Y))
       sel(0,cons(X,Y)) -> X
       sel(s(N),cons(X,Y)) -> sel(N,activate(Y))
       fib1(X1,X2) -> n__fib1(X1,X2)
       activate(n__fib1(X1,X2)) -> fib1(X1,X2)
       activate(X) -> X
       

   is terminating (use RPOS with AProVE).
2. The µ-termination of Ex8_BLR02 can also be proved by using Ferreira and Ribeiro's transformation. The TRS Ex8_BLR02_FR:

       fib(N) -> sel(N,fib1(s(0),s(0)))
       fib1(X,Y) -> cons(X,n__fib1(Y,n__add(X,Y)))
       add(0,X) -> X
       add(s(X),Y) -> s(add(X,Y))
       sel(0,cons(X,XS)) -> X
       sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
       fib1(X1,X2) -> n__fib1(X1,X2)
       add(X1,X2) -> n__add(X1,X2)
       activate(n__fib1(X1,X2)) -> fib1(activate(X1),activate(X2))
       activate(n__add(X1,X2)) -> add(activate(X1),activate(X2))
       activate(X) -> X
       

   is terminating (use RPOS with AProVE).
3. By [GM04, Theorem 22], the µ-termination of Ex8_BLR02 can also be proved by using Giesl and Middeldorp's transformation (but no concrete proof has been reported yet).
4. The µ-termination of Ex8_BLR02 can be proved by CSRPO together with the following [BLR02, Example 8] and automatically by MuTerm:
   • marking map:

            m(cons,2)=m(_cons,2)={fib1}
            

   • precedence:

            fib > sel, fib1, s 0
            sel > fib1 > cons, add, _fib1
            add > s
            

   • status:

            st(sel)=lex; 
            st(f)=mul for all other symbols f.